Search Results

Documents authored by Gowers, W. John

Found 3 Possible Name Variants:

Gowers, W. John

Document
DOI: 10.4230/LIPIcs.CSL.2018.24
A Fully Abstract Game Semantics for Countable Nondeterminism

Authors: W. John Gowers and James D. Laird

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
The concept of fairness for a concurrent program means that the program must be able to exhibit an unbounded amount of nondeterminism without diverging. Game semantics models of nondeterminism show that this is hard to implement; for example, Harmer and McCusker's model only admits infinite nondeterminism if there is also the possibility of divergence. We solve a long standing problem by giving a fully abstract game semantics for a simple stateful language with a countably infinite nondeterminism primitive. We see that doing so requires us to keep track of infinitary information about strategies, as well as their finite behaviours. The unbounded nondeterminism gives rise to further problems, which can be formalized as a lack of continuity in the language. In order to prove adequacy for our model (which usually requires continuity), we develop a new technique in which we simulate the nondeterminism using a deterministic stateful construction, and then use combinatorial techniques to transfer the result to the nondeterministic language. Lastly, we prove full abstraction for the model; because of the lack of continuity, we cannot deduce this from definability of compact elements in the usual way, and we have to use a stronger universality result instead. We discuss how our techniques yield proofs of adequacy for models of nondeterministic PCF, such as those given by Tsukada and Ong.
Cite as

W. John Gowers and James D. Laird. A Fully Abstract Game Semantics for Countable Nondeterminism. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{gowers_et_al:LIPIcs.CSL.2018.24,
  author =	{Gowers, W. John and Laird, James D.},
  title =	{{A Fully Abstract Game Semantics for Countable Nondeterminism}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.24},
  URN =		{urn:nbn:de:0030-drops-96918},
  doi =		{10.4230/LIPIcs.CSL.2018.24},
  annote =	{Keywords: semantics, nondeterminism, games and logic}
}

Gowers, William John

Document
DOI: 10.4230/LIPIcs.CALCO.2017.13
Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics

Authors: William John Gowers and James Laird

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract
The non-commutative sequoid operator (/) on games was introduced to capture algebraically the presence of state in history-sensitive strategies in game semantics, by imposing a causality relation on the tensor product of games. Coalgebras for the functor A (/) _ - i.e., morphisms from S to A (/) S --- may be viewed as state transformers: if A (/) _ has a final coalgebra, !A, then the anamorphism of such a state transformer encapsulates its explicit state, so that it is shared only between successive invocations. We study the conditions under which a final coalgebra !A for A (/) _ is the carrier of a cofree commutative comonoid on A. That is, it is a model of the exponential of linear logic in which we can construct imperative objects such as reference cells coalgebraically, in a game semantics setting. We show that if the tensor decomposes into the sequoid, the final coalgebra !A may be endowed with the structure of the cofree commutative comonoid if there is a natural isomorphism from !(A × B)to !A (x) !B. This condition is always satisfied if !A is the bifree algebra for A (/) _, but in general it is necessary to impose it, as we establish by giving an example of a sequoidally decomposable category of games in which plays will be allowed to have transfinite length. In this category, the final coalgebra for the functor A (/)_ is not the cofree commutative comonoid over A: we illustrate this by explicitly contrasting the final sequence for the functor A (/) _ with the chain of symmetric tensor powers used in the construction of the cofree commutative comonoid as a limit by Melliès, Tabareau and Tasson.
Cite as

William John Gowers and James Laird. Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{gowers_et_al:LIPIcs.CALCO.2017.13,
  author =	{Gowers, William John and Laird, James},
  title =	{{Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.13},
  URN =		{urn:nbn:de:0030-drops-80454},
  doi =		{10.4230/LIPIcs.CALCO.2017.13},
  annote =	{Keywords: Game Semantics, Stateful Languages, Transfinite Games, Sequoid Operator}
}

Gowers, W. T.

Document
DOI: 10.4230/LIPIcs.ITCS.2022.80
Mixing in Non-Quasirandom Groups

Authors: W. T. Gowers and Emanuele Viola

Published in: LIPIcs, Volume 215, 13th Innovations in Theoretical Computer Science Conference (ITCS 2022)

Abstract
We initiate a systematic study of mixing in non-quasirandom groups. Let A and B be two independent, high-entropy distributions over a group G. We show that the product distribution AB is statistically close to the distribution F(AB) for several choices of G and F, including: 1) G is the affine group of 2x2 matrices, and F sets the top-right matrix entry to a uniform value, 2) G is the lamplighter group, that is the wreath product of ℤ₂ and ℤ_{n}, and F is multiplication by a certain subgroup, 3) G is Hⁿ where H is non-abelian, and F selects a uniform coordinate and takes a uniform conjugate of it. The obtained bounds for (1) and (2) are tight. This work is motivated by and applied to problems in communication complexity. We consider the 3-party communication problem of deciding if the product of three group elements multiplies to the identity. We prove lower bounds for the groups above, which are tight for the affine and the lamplighter groups.
Cite as

W. T. Gowers and Emanuele Viola. Mixing in Non-Quasirandom Groups. In 13th Innovations in Theoretical Computer Science Conference (ITCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 215, pp. 80:1-80:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gowers_et_al:LIPIcs.ITCS.2022.80,
  author =	{Gowers, W. T. and Viola, Emanuele},
  title =	{{Mixing in Non-Quasirandom Groups}},
  booktitle =	{13th Innovations in Theoretical Computer Science Conference (ITCS 2022)},
  pages =	{80:1--80:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-217-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{215},
  editor =	{Braverman, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2022.80},
  URN =		{urn:nbn:de:0030-drops-156761},
  doi =		{10.4230/LIPIcs.ITCS.2022.80},
  annote =	{Keywords: Groups, representation theory, mixing, communication complexity, quasi-random}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.4
A Graphical User Interface Framework for Formal Verification

Authors: Edward W. Ayers, Mateja Jamnik, and W. T. Gowers

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
We present the "ProofWidgets" framework for implementing general user interfaces (UIs) within an interactive theorem prover. The framework uses web technology and functional reactive programming, as well as metaprogramming features of advanced interactive theorem proving (ITP) systems to allow users to create arbitrary interactive UIs for representing the goal state. Users of the framework can create GUIs declaratively within the ITP’s metaprogramming language, without having to develop in multiple languages and without coordinated changes across multiple projects, which improves development time for new designs of UI. The ProofWidgets framework also allows UIs to make use of the full context of the theorem prover and the specialised libraries that ITPs offer, such as methods for dealing with expressions and tactics. The framework includes an extensible structured pretty-printing engine that enables advanced interaction with expressions such as interactive term rewriting. We exemplify the framework with an implementation for the https://leanprover-community.github.io. The framework is already in use by hundreds of contributors to the Lean mathematical library.
Cite as

Edward W. Ayers, Mateja Jamnik, and W. T. Gowers. A Graphical User Interface Framework for Formal Verification. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{ayers_et_al:LIPIcs.ITP.2021.4,
  author =	{Ayers, Edward W. and Jamnik, Mateja and Gowers, W. T.},
  title =	{{A Graphical User Interface Framework for Formal Verification}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{4:1--4:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.4},
  URN =		{urn:nbn:de:0030-drops-138996},
  doi =		{10.4230/LIPIcs.ITP.2021.4},
  annote =	{Keywords: User Interfaces, ITP}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact